Nuprl Lemma : R-Dsys-Rplus
0,22
postcript
pdf
A
,
B
:Top. [[
A
B
]] ~ ([[
A
]]
[[
B
]])
latex
Definitions
x
:
A
.
B
(
x
)
,
[[
R
]]
,
t
T
Lemmas
top
wf
origin
A, B:Top. [[A 
B]] ~ ([[A]] [[B]]) A, B:Top. [[A B]] ~ ([[A]] [[B]]) x:A. B(x)
T